Section: New Results

Automated Deduction

• In his thesis [14] , S. Lescuyer formalized and designed purely reflexive tactics for automated deduction in Coq.

• É. Contejean, together with Pierre Courtieu, Julien Forest, Olivier Pons and Xavier Urbain (Cedric Laboratory, CNAM & ENSIIE) presented the last version of the rewriting toolkit CiME3 at RTA 2011 [25] . Amongst other original features, this version enjoys two kinds of engines: to handle and discover proofs of various properties of rewriting systems, and to generate Coq scripts from proof traces given in certification problem format in order to certify them with a skeptical proof assistant like Coq. Thus, these features open the way for using CiME3 to add automation to proofs of termination or confluence in a formal development in the Coq proof assistant.

• In their TACAS paper [24] , S. Conchon, É. Contejean and M. Iguernelala present a modular extension of ground AC-completion for deciding formulas in the combination of the theory of equality with user-defined AC symbols, uninterpreted symbols and an arbitrary signature disjoint Shostak theory X.

• F. Bobot and A. Paskevich studied translation from a first-order logic with polymorphic types à la ML (which is the base logic of the Why platform and the Alt-Ergo theorem prover) to a many-sorted or one-sorted logic implemented in mainstream automated theorem provers. They devised a three-stage scheme where the last stage eliminates polymorphic types while adding the necessary “annotations” to preserve soundness, and the first two stages serve to protect certain terms so that they can keep their original types and unannotated form. Such protection allows to make use of provers' built-in theories and operations. This work generalizes the previous study by S. Lescuyer and J.-F. Couchot [65] onto arbitrary monomorphic types, e.g. array types. It was presented at FroCoS 2011 [22] (see also an extended version with full proofs [42] ). These results are part of F. Bobot's PhD thesis [12] .